es:ES, i:Id, P:(state@iProp).
@i stable state.P(state)    e@i. P((state when e))  e'e.P(state after e') 

latex

Definitions	x(s), x:A. B(x), b, P  Q, False, A, t  T, e@i. P(e), @i stable state.P(state)  , P & Q, (e <loc e'), True, T, Id, ES, state@i, state after e, e  e' , Prop, E, {T}, x. t(x), WellFnd{i}(A;x,y.R(x;y)), (state when e), loc(e), e'e.P(e'), A & B, P  Q, P  Q, 1of(t), pred(e), SQType(T), P  Q
Lemmas	state-after-pred, Id sq, es-pred wf, es-pred-locl, es-le-iff, event system wf, Id wf, es-stable wf, es-E wf, es-loc wf, es-state-when wf, squash wf, true wf, es-locl-wellfnd, es-locl wf, es-le wf, es-state-after wf, es-state wf, es-le-loc, es-loc-pred